| Definitions | x:A  B(x),  x:A. B(x), fpf(A; a.B(a)), Type, type List, ecl-trans-normal(x), event-info(ds;da), left + right, ma-valtype(da; k),  , t  T, decl-state(ds), Knd, (x l), {x:A| B(x)} ,  , x:A  B(x),  , s = t, <a, b>, ecl-trans-tuple{i:l}(ds; da), prop{i:l}, ecl-trans-type(A), fpf-cap(f; eq; x; z), strong-subtype(A; B), P   Q, subtype(S; T), ecl-trans-state(v; L), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), let x = a in b(x), combine-ecl-tuples2(A; B; f; g),  x:A. B(x), Unit, iseg(T; l1; l2), ecl-trans-halt2(ds; da; A), f(a), int_seg(i; j), void, P  Q, P  Q,  b, False,  A, isl(x), P Q, ff, inl x , #$n, n + m, tt, merge(as; bs), t.2, t.1, Kind-deq, deq-member(eq; x; L), if b then t else f fi , bor(p; q),  x.A(x), reduce(f; k; as), combine-halt-info(ea; eb; f; g; x),  , inr x , append(as; bs), [], cons(car; cdr), A  B, a < b,  , lelt(i; j; k), p-outcome(p), decision, grp_car(g), ecl-trans-es(v), guard(T),  x. t(x), Id, ecl-trans-init(v), ecl-trans-state-from(v; z; L), case b of inl(x) => s(x) | inr(y) => t(y), decidable(P), P  Q, ecl-trans-h(v), axiom, listp(A), isect(A; x.B(x)), top, sqequal(s; t), divides(b; a), assoced(a; b), set_leq(p; a; b), set_lt(p; a; b), grp_lt(g; a; b), A c B, x f y, l_all(L; T; x.P(x)), l_exists(L; T; x.P(x)), qle(r; s), qless(r; s), q-rel(r; x), l_disjoint(T; l1; l2), es-locl(es; e; e'), es-le(es; e; e'), es-causl(es; e; e'), e c e', e<e'.P(e), ee'.P(e), e<e'.P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), es-r-immediate-pred(es; R; e'; e), same-thread(es; p; e; e'), snd-it(ff; p; e; i; j), rcv-it(ff; p; e; i; j), f2f+-pred{i:l}(es; ff; f2f+; sndr; rcvr; e'; e),  b, compat(T; l1; l2), True, let x,y = A in B(x;y), bimplies(p; q), band(p; q), i <z j, i z j, sorted(L), no_repeats(T; l), priority-select(f; g; as), eqof(d), nat-deq, ge(i; j), sq_type(T),  T, ||as||, l[i], (i = j), EqDecider(T), if a=b then c else d, IdLnk, fpf-single(x; v), fpf-join(eq; f; g), finite-type(T), fpf-sub(A; a.B(a); eq; f; g), loc(e), es-vartype(es; i; x), es-state(es; i), Namer(n; Id_list), interface(ds; da; A), ma-state(ds), fpf-dom(eq; x; f), eq_bool(p; q), eq_atom(x; y), null(as), set_blt(p; a; b), set_le(p), set_eq(p), grp_blt(g; a; b), grp_eq(g), rng_eq(r), dcdr-to-bool(d), eq_atom{$n:n}(x; y), q_le(r; s), q_less(a; b), qeq(r; s), eq_lnk(a; b), eq_id(a; b), int_nzero, rationals, atom, quotient(A; x,y.B(x;y)), set_car(p), rng_car(r), atom{$n:n}, dstype(TypeNames; d; a), MaName, es-E(es) |
| Lemmas | guard wf, rev implies wf, bnot thru bor, sorted wf, priority-select-inr, priority-select-property, deq wf, IdLnk wf, l all wf2, not-isl-priority-select, priority-select-ff, member-merge, cons member, decidable int equal, iseg append single, true wf, squash wf, iseg weakening, or functionality wrt iff, assert of bor, and functionality wrt iff, assert of band, non neg length, select wf, length wf1, no repeats-merge, no repeats cons, sorted-merge, sorted-cons, subtype rel list, band wf, bor wf, l exists wf, nat-deq wf, eqof wf, priority-select wf, priority-select-tt, iff functionality wrt iff, merge wf, ifthenelse wf, combine-halt-info wf, decidable lt, decidable le, common iseg compat, iseg append, fpf-cap wf, member append, bnot wf, Kind-deq wf, deq-member wf, assert-deq-member, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, decidable assert, ecl-trans-state-append, top wf, append wf, ecl-trans-state-from wf, iseg nil, decidable false, false wf, it wf, ecl-trans-es wf, nat plus inc, ecl-trans-normal wf, fpf wf, Id wf, last induction, btrue wf, bfalse wf, le wf, isl wf, not wf, combine-ecl-tuples2 wf, ecl-trans-type wf, assert wf, int seg wf, ecl-trans-halt2 wf, iseg wf, event-info wf, iff wf, unit wf, ecl-trans-state wf, member wf, ecl-trans-tuple wf, nat plus wf, nat wf, l member wf, Knd wf, decl-state wf, bool wf, ma-valtype wf, subtype rel wf, subtype rel self |
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple(ds; da).